basic
RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f) == x, y:T. R(x;y)  R'(f(x);f(y)) 

latex

---

clarification:

basic
RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f) == x:T, y:T. R(x;y)  R'(f(x);f(y)) 

latex

Up	gen algebra 1
Wellformedness Lemmas	rels iso wf
Definitions	x:A. B(x), P  Q